7e8b66c5f6a195bd5da7b53986405cda912c8896,src/main/java/org/basex/gui/editor/SearchPanel.java,SearchPanel,activate,#String#,203
Before Change
if(button != null) button.setSelected(true);
}
if(string == null) {
search.requestFocusInWindow();
} else if(!new SearchContext(this, search.getText()).matches(string)) {
// set new, different search string
search.setText(string);
After Change
setVisible(true);
if(button != null) button.setSelected(true);
}
if(focus) search.requestFocusInWindow();
// set new, different search string
if(string != null && !new SearchContext(this, search.getText()).matches(string)) {